T:Type, P:(T), as:T List, d:Top.
(a:T. (a  as) & P(a))  (first a  as s.t. P(a) else d) = hd(filter(a.P(a);as))  T 

latex

Definitions	P  Q, A & B, Unit, b, A, {T}, P  Q, False, , first x  as s.t. P(x) else d, hd(l), Top, P  Q, x:A. B(x), P & Q, (x  l), Prop, b, x:A. B(x), x(s), t  T
Lemmas	assert wf, l member wf, top wf, bool wf, nil member, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, cons member